Iof proof for Lemma complete nat ind:
1. P :
{k}
2.
i:. (j:i. P(j)) 
P(i)
3. i :
P(i)
by PERMUTE{1:n,
by PERMUTE{2:n,
by PERMUTE{3:n,
by PERMUTE{4:n,
by PERMUTE{5:n,
by PERMUTE{6:n,
by PERMUTE{7:n,
by PERMUTE{8:n,
by PERMUTE{9:n,
by PERMUTE{10:n,
by PERMUTE{11:n,
by PERMUTE{12:n,
by PERMUTE{13:n,
by PERMUTE{14:n,
by PERMUTE{5:n,
by PERMUTE{15:n,
by PERMUTE{16:n,
by PERMUTE{17:n}
1: .....arith..... NILNIL
1: 3. zz : 
1: 4. zz < 0
1: 5. ((zz + 1) 
0 ) (i:. (i < (zz + 1)) P(i))
1: 6. zz 0
1: i:. (i < zz) P(i)
2: .....wf..... NILNIL
2: 3. zz :
2: 4. zz < 0
2: 5. ((zz + 1) 0 ) (i:. (i < (zz + 1)) P(i))
2: (zz 0 ) 
3:
3: 4. i < 0
3: P(i)
4: .....wf..... NILNIL
4: (i < 0)
5: .....wf..... NILNIL
5: 2. i:. (j:i. P(j)) P(i)
5: Type
6: .....wf..... NILNIL
6: 2. i:. (j:i. P(j)) P(i)
6: (0 0 )
7: .....arith..... NILNIL
7: 3. zz :
7: 4. 0 < zz
7: 5. zz 0
7: (zz - 1) 0
8: .....wf..... NILNIL
8: 3. zz :
8: 4. 0 < zz
8: 5. i :
8: 6. i < zz
8: 7. i1 : i
8: i1
9:
9: 3. zz :
9: 4. 0 < zz
9: 5. i :
9: 6. i < zz
9: 7. i1 : i
9: i1 < (zz - 1)
10: .....wf..... NILNIL
10: 3. zz :
10: 4. 0 < zz
10: 5. i:. (i < (zz - 1)) P(i)
10: 6. i :
10: 7. i < zz
10: i Type
11:
11: 4. i1:i. P(i1)
11: P(i)
12: .....wf..... NILNIL
12: 3. zz :
12: 4. 0 < zz
12: 5. i:. (i < (zz - 1)) P(i)
12: 6. i :
12: (i < zz)
13: .....wf..... NILNIL
13: 3. zz :
13: 4. 0 < zz
13: 5. i:. (i < (zz - 1)) P(i)
13: Type
14: .....wf..... NILNIL
14: 3. zz :
14: 4. 0 < zz
14: 5. ((zz - 1) 0 ) (i:. (i < (zz - 1)) P(i))
14: (zz 0 )
15: .....wf..... NILNIL
15: (i + 1)
16: .....wf..... NILNIL
16: i
17: .....arith..... NILNIL
17: i < (i + 1)
.
B
}